(set-logic QF_BV)
(declare-fun _substvar_51_ () (_ BitVec 1))
(declare-fun _substvar_84_ () Bool)
(declare-fun _substvar_41_ () (_ BitVec 4))
(declare-fun _substvar_52_ () (_ BitVec 1))
(declare-fun _substvar_47_ () (_ BitVec 4))
(assert (= _substvar_41_ _substvar_47_))
(assert (= _substvar_52_ (ite (= (_ bv0 4) _substvar_41_) (_ bv1 1) (_ bv0 1))))
(assert (= _substvar_51_ (ite _substvar_84_ _substvar_52_ (_ bv1 1))))
(check-sat)
(exit)
